

LEMMA

If x partially overlaps y and y is a non-tangential proper part of z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (po c1042696 c1042695)) v (~ (ntpp c1042695 c1042694))) v (~ (p c1042694 c1042696)))


> hypdisj
=============================
Step 3

? (~ (p c1042694 c1042696))

1. (ntpp c1042695 c1042694)
2. (po c1042696 c1042695)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var43 c1042694)
|
|1. (p c1042694 c1042696)
|2. (ntpp c1042695 c1042694)
|3. (po c1042696 c1042695)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var46 c1042694)
||
||1. (~ (c Var43 c1042694))
||2. (p c1042694 c1042696)
||3. (ntpp c1042695 c1042694)
||4. (po c1042696 c1042695)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 6
||
||? (pp Var46 c1042694)
||
||1. (~ (p Var46 c1042694))
||2. (~ (c Var43 c1042694))
||3. (p c1042694 c1042696)
||4. (ntpp c1042695 c1042694)
||5. (po c1042696 c1042695)
||
||> ((pp X Y) <-- (ntpp X Y))
||=============================
||Step 7
||
||? (ntpp Var46 c1042694)
||
||1. (~ (pp Var46 c1042694))
||2. (~ (p Var46 c1042694))
||3. (~ (c Var43 c1042694))
||4. (p c1042694 c1042696)
||5. (ntpp c1042695 c1042694)
||6. (po c1042696 c1042695)
||
||> hyp
|=============================
|Step 8
|
|? (c (f1037643 c1042695 Var55 Var56) c1042695)
|
|1. (~ (c (f1037643 c1042695 Var55 Var56) c1042694))
|2. (p c1042694 c1042696)
|3. (ntpp c1042695 c1042694)
|4. (po c1042696 c1042695)
|
|> ((c (f1037643 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p c1042695 Var55))
|
|1. (~ (c (f1037643 c1042695 Var55 Var56) c1042695))
|2. (~ (c (f1037643 c1042695 Var55 Var56) c1042694))
|3. (p c1042694 c1042696)
|4. (ntpp c1042695 c1042694)
|5. (po c1042696 c1042695)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 10
|
|? (po Var55 c1042695)
|
|1. (p c1042695 Var55)
|2. (~ (c (f1037643 c1042695 Var55 Var56) c1042695))
|3. (~ (c (f1037643 c1042695 Var55 Var56) c1042694))
|4. (p c1042694 c1042696)
|5. (ntpp c1042695 c1042694)
|6. (po c1042696 c1042695)
|
|> hyp
=============================
Step 11

? (~ (c (f1037643 c1042695 c1042696 Var56) c1042696))

1. (p c1042694 c1042696)
2. (ntpp c1042695 c1042694)
3. (po c1042696 c1042695)

> ((~ (c (f1037643 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 12

? (~ (p c1042695 c1042696))

1. (c (f1037643 c1042695 c1042696 Var56) c1042696)
2. (p c1042694 c1042696)
3. (ntpp c1042695 c1042694)
4. (po c1042696 c1042695)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 13

? (po c1042696 c1042695)

1. (p c1042695 c1042696)
2. (c (f1037643 c1042695 c1042696 Var56) c1042696)
3. (p c1042694 c1042696)
4. (ntpp c1042695 c1042694)
5. (po c1042696 c1042695)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c1047925 c1047924)) v (o c1047925 c1047924))


> hypdisj
=============================
Step 3

? (o c1047925 c1047924)

1. (po c1047925 c1047924)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c1047925 c1047924)

1. (~ (o c1047925 c1047924))
2. (po c1047925 c1047924)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c1053210 c1053209)) v (c c1053210 c1053209))


> hypdisj
=============================
Step 3

? (c c1053210 c1053209)

1. (o c1053210 c1053209)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c1053209)
|
|1. (~ (c c1053210 c1053209))
|2. (o c1053210 c1053209)
|
|> ((p Z X) <-- (~ (c (f1047957 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f1047957 Var48 c1053209 Var51) Var48))
|
|1. (~ (p Var48 c1053209))
|2. (~ (c c1053210 c1053209))
|3. (o c1053210 c1053209)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f1047974 Var57 Var54) Var54)
||
||1. (c (f1047957 (f1047974 Var57 Var54) c1053209 Var51) (f1047974 Var57 Var54))
||2. (~ (p (f1047974 Var57 Var54) c1053209))
||3. (~ (c c1053210 c1053209))
||4. (o c1053210 c1053209)
||
||> ((p (f1047974 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f1047974 Var57 Var54) Var54))
||2. (c (f1047957 (f1047974 Var57 Var54) c1053209 Var51) (f1047974 Var57 Var54))
||3. (~ (p (f1047974 Var57 Var54) c1053209))
||4. (~ (c c1053210 c1053209))
||5. (o c1053210 c1053209)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f1047957 (f1047974 c1053210 c1053209) c1053209 Var51) c1053209))
|
|1. (c (f1047957 (f1047974 c1053210 c1053209) c1053209 Var51) (f1047974 c1053210 c1053209))
|2. (~ (p (f1047974 c1053210 c1053209) c1053209))
|3. (~ (c c1053210 c1053209))
|4. (o c1053210 c1053209)
|
|> ((~ (c (f1047957 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f1047974 c1053210 c1053209) c1053209))
|
|1. (c (f1047957 (f1047974 c1053210 c1053209) c1053209 Var51) c1053209)
|2. (c (f1047957 (f1047974 c1053210 c1053209) c1053209 Var51) (f1047974 c1053210 c1053209))
|3. (~ (p (f1047974 c1053210 c1053209) c1053209))
|4. (~ (c c1053210 c1053209))
|5. (o c1053210 c1053209)
|
|> hyp
=============================
Step 10

? (c c1053210 (f1047974 c1053210 c1053209))

1. (~ (c c1053210 c1053209))
2. (o c1053210 c1053209)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f1047974 c1053210 c1053209) c1053210)

1. (~ (c c1053210 (f1047974 c1053210 c1053209)))
2. (~ (c c1053210 c1053209))
3. (o c1053210 c1053209)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f1047974 c1053210 Var71) c1053210)
|
|1. (~ (c (f1047974 c1053210 c1053209) c1053210))
|2. (~ (c c1053210 (f1047974 c1053210 c1053209)))
|3. (~ (c c1053210 c1053209))
|4. (o c1053210 c1053209)
|
|> ((p (f1047974 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c1053210 Var71)
|
|1. (~ (p (f1047974 c1053210 Var71) c1053210))
|2. (~ (c (f1047974 c1053210 c1053209) c1053210))
|3. (~ (c c1053210 (f1047974 c1053210 c1053209)))
|4. (~ (c c1053210 c1053209))
|5. (o c1053210 c1053209)
|
|> hyp
=============================
Step 14

? (c (f1047974 c1053210 c1053209) (f1047974 c1053210 c1053209))

1. (~ (c (f1047974 c1053210 c1053209) c1053210))
2. (~ (c c1053210 (f1047974 c1053210 c1053209)))
3. (~ (c c1053210 c1053209))
4. (o c1053210 c1053209)

> ((c X X) <--)


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c1058551 c1058550)) v (pp c1058551 c1058550))


> hypdisj
=============================
Step 3

? (pp c1058551 c1058550)

1. (ntpp c1058551 c1058550)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c1058551 c1058550)

1. (~ (pp c1058551 c1058550))
2. (ntpp c1058551 c1058550)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c1063948 c1063947)) v (p c1063948 c1063947))


> hypdisj
=============================
Step 3

? (p c1063948 c1063947)

1. (pp c1063948 c1063947)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c1063948 c1063947)

1. (~ (p c1063948 c1063947))
2. (pp c1063948 c1063947)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c1069403 c1069402)) v (~ (c c1069401 c1069403))) v (c c1069401 c1069402))


> hypdisj
=============================
Step 3

? (c c1069401 c1069402)

1. (c c1069401 c1069403)
2. (p c1069403 c1069402)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c1069402)
|
|1. (~ (c c1069401 c1069402))
|2. (c c1069401 c1069403)
|3. (p c1069403 c1069402)
|
|> hyp
=============================
Step 5

? (c c1069401 c1069403)

1. (~ (c c1069401 c1069402))
2. (c c1069401 c1069403)
3. (p c1069403 c1069402)

> hyp


LEMMA

From po(x,y) and ntpp(y,z), x is connected to z.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp y z)) => (c x z)))))


> revsk
=============================
Step 2

? (((~ (po c1075014 c1075013)) v (~ (ntpp c1075013 c1075012))) v (c c1075014 c1075012))


> hypdisj
=============================
Step 3

? (c c1075014 c1075012)

1. (ntpp c1075013 c1075012)
2. (po c1075014 c1075013)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var32 c1075012)
|
|1. (~ (c c1075014 c1075012))
|2. (ntpp c1075013 c1075012)
|3. (po c1075014 c1075013)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 5
|
|? (pp Var32 c1075012)
|
|1. (~ (p Var32 c1075012))
|2. (~ (c c1075014 c1075012))
|3. (ntpp c1075013 c1075012)
|4. (po c1075014 c1075013)
|
|> ((pp X Y) <-- (ntpp X Y))
|=============================
|Step 6
|
|? (ntpp Var32 c1075012)
|
|1. (~ (pp Var32 c1075012))
|2. (~ (p Var32 c1075012))
|3. (~ (c c1075014 c1075012))
|4. (ntpp c1075013 c1075012)
|5. (po c1075014 c1075013)
|
|> hyp
=============================
Step 7

? (c c1075014 c1075013)

1. (~ (c c1075014 c1075012))
2. (ntpp c1075013 c1075012)
3. (po c1075014 c1075013)

> ((c X Y) <-- (o X Y))
=============================
Step 8

? (o c1075014 c1075013)

1. (~ (c c1075014 c1075013))
2. (~ (c c1075014 c1075012))
3. (ntpp c1075013 c1075012)
4. (po c1075014 c1075013)

> ((o X Y) <-- (po X Y))
=============================
Step 9

? (po c1075014 c1075013)

1. (~ (o c1075014 c1075013))
2. (~ (c c1075014 c1075013))
3. (~ (c c1075014 c1075012))
4. (ntpp c1075013 c1075012)
5. (po c1075014 c1075013)

> hyp


LEMMA

Classify x,z as ec or po or pp.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp y z)) => ((ec x z) v ((po x z) v (pp x z)))))))


> revsk
=============================
Step 2

? (((~ (po c1080781 c1080780)) v (~ (ntpp c1080780 c1080779))) v ((ec c1080781 c1080779) v ((po c1080781 c1080779) v (pp c1080781 c1080779))))


> hypdisj
=============================
Step 3

? (pp c1080781 c1080779)

1. (~ (po c1080781 c1080779))
2. (~ (ec c1080781 c1080779))
3. (ntpp c1080780 c1080779)
4. (po c1080781 c1080780)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c1080781 c1080779)
|
|1. (~ (pp c1080781 c1080779))
|2. (~ (po c1080781 c1080779))
|3. (~ (ec c1080781 c1080779))
|4. (ntpp c1080780 c1080779)
|5. (po c1080781 c1080780)
|
|> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
|||=============================
|||Step 5
|||
|||? (o c1080781 c1080779)
|||
|||1. (~ (p c1080781 c1080779))
|||2. (~ (pp c1080781 c1080779))
|||3. (~ (po c1080781 c1080779))
|||4. (~ (ec c1080781 c1080779))
|||5. (ntpp c1080780 c1080779)
|||6. (po c1080781 c1080780)
|||
|||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
||||=============================
||||Step 6
||||
||||? (c c1080781 c1080779)
||||
||||1. (~ (o c1080781 c1080779))
||||2. (~ (p c1080781 c1080779))
||||3. (~ (pp c1080781 c1080779))
||||4. (~ (po c1080781 c1080779))
||||5. (~ (ec c1080781 c1080779))
||||6. (ntpp c1080780 c1080779)
||||7. (po c1080781 c1080780)
||||
||||> ((c X Z) <-- (po X Y) (ntpp Y Z))
|||||=============================
|||||Step 7
|||||
|||||? (po c1080781 Var67)
|||||
|||||1. (~ (c c1080781 c1080779))
|||||2. (~ (o c1080781 c1080779))
|||||3. (~ (p c1080781 c1080779))
|||||4. (~ (pp c1080781 c1080779))
|||||5. (~ (po c1080781 c1080779))
|||||6. (~ (ec c1080781 c1080779))
|||||7. (ntpp c1080780 c1080779)
|||||8. (po c1080781 c1080780)
|||||
|||||> hyp
||||=============================
||||Step 8
||||
||||? (ntpp c1080780 c1080779)
||||
||||1. (~ (c c1080781 c1080779))
||||2. (~ (o c1080781 c1080779))
||||3. (~ (p c1080781 c1080779))
||||4. (~ (pp c1080781 c1080779))
||||5. (~ (po c1080781 c1080779))
||||6. (~ (ec c1080781 c1080779))
||||7. (ntpp c1080780 c1080779)
||||8. (po c1080781 c1080780)
||||
||||> hyp
|||=============================
|||Step 9
|||
|||? (~ (ec c1080781 c1080779))
|||
|||1. (~ (o c1080781 c1080779))
|||2. (~ (p c1080781 c1080779))
|||3. (~ (pp c1080781 c1080779))
|||4. (~ (po c1080781 c1080779))
|||5. (~ (ec c1080781 c1080779))
|||6. (ntpp c1080780 c1080779)
|||7. (po c1080781 c1080780)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (p c1080779 c1080781))
||
||1. (~ (p c1080781 c1080779))
||2. (~ (pp c1080781 c1080779))
||3. (~ (po c1080781 c1080779))
||4. (~ (ec c1080781 c1080779))
||5. (ntpp c1080780 c1080779)
||6. (po c1080781 c1080780)
||
||> ((~ (p Z X)) <-- (po X Y) (ntpp Y Z))
|||=============================
|||Step 11
|||
|||? (po c1080781 Var73)
|||
|||1. (p c1080779 c1080781)
|||2. (~ (p c1080781 c1080779))
|||3. (~ (pp c1080781 c1080779))
|||4. (~ (po c1080781 c1080779))
|||5. (~ (ec c1080781 c1080779))
|||6. (ntpp c1080780 c1080779)
|||7. (po c1080781 c1080780)
|||
|||> hyp
||=============================
||Step 12
||
||? (ntpp c1080780 c1080779)
||
||1. (p c1080779 c1080781)
||2. (~ (p c1080781 c1080779))
||3. (~ (pp c1080781 c1080779))
||4. (~ (po c1080781 c1080779))
||5. (~ (ec c1080781 c1080779))
||6. (ntpp c1080780 c1080779)
||7. (po c1080781 c1080780)
||
||> hyp
|=============================
|Step 13
|
|? (~ (po c1080781 c1080779))
|
|1. (~ (p c1080781 c1080779))
|2. (~ (pp c1080781 c1080779))
|3. (~ (po c1080781 c1080779))
|4. (~ (ec c1080781 c1080779))
|5. (ntpp c1080780 c1080779)
|6. (po c1080781 c1080780)
|
|> hyp
=============================
Step 14

? (~ (p c1080779 c1080781))

1. (~ (pp c1080781 c1080779))
2. (~ (po c1080781 c1080779))
3. (~ (ec c1080781 c1080779))
4. (ntpp c1080780 c1080779)
5. (po c1080781 c1080780)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 15
|
|? (c Var79 c1080779)
|
|1. (p c1080779 c1080781)
|2. (~ (pp c1080781 c1080779))
|3. (~ (po c1080781 c1080779))
|4. (~ (ec c1080781 c1080779))
|5. (ntpp c1080780 c1080779)
|6. (po c1080781 c1080780)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 16
||
||? (p Var82 c1080779)
||
||1. (~ (c Var79 c1080779))
||2. (p c1080779 c1080781)
||3. (~ (pp c1080781 c1080779))
||4. (~ (po c1080781 c1080779))
||5. (~ (ec c1080781 c1080779))
||6. (ntpp c1080780 c1080779)
||7. (po c1080781 c1080780)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 17
||
||? (pp Var82 c1080779)
||
||1. (~ (p Var82 c1080779))
||2. (~ (c Var79 c1080779))
||3. (p c1080779 c1080781)
||4. (~ (pp c1080781 c1080779))
||5. (~ (po c1080781 c1080779))
||6. (~ (ec c1080781 c1080779))
||7. (ntpp c1080780 c1080779)
||8. (po c1080781 c1080780)
||
||> ((pp X Y) <-- (ntpp X Y))
||=============================
||Step 18
||
||? (ntpp Var82 c1080779)
||
||1. (~ (pp Var82 c1080779))
||2. (~ (p Var82 c1080779))
||3. (~ (c Var79 c1080779))
||4. (p c1080779 c1080781)
||5. (~ (pp c1080781 c1080779))
||6. (~ (po c1080781 c1080779))
||7. (~ (ec c1080781 c1080779))
||8. (ntpp c1080780 c1080779)
||9. (po c1080781 c1080780)
||
||> hyp
|=============================
|Step 19
|
|? (c (f1075070 c1080780 Var91 Var92) c1080780)
|
|1. (~ (c (f1075070 c1080780 Var91 Var92) c1080779))
|2. (p c1080779 c1080781)
|3. (~ (pp c1080781 c1080779))
|4. (~ (po c1080781 c1080779))
|5. (~ (ec c1080781 c1080779))
|6. (ntpp c1080780 c1080779)
|7. (po c1080781 c1080780)
|
|> ((c (f1075070 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 20
|
|? (~ (p c1080780 Var91))
|
|1. (~ (c (f1075070 c1080780 Var91 Var92) c1080780))
|2. (~ (c (f1075070 c1080780 Var91 Var92) c1080779))
|3. (p c1080779 c1080781)
|4. (~ (pp c1080781 c1080779))
|5. (~ (po c1080781 c1080779))
|6. (~ (ec c1080781 c1080779))
|7. (ntpp c1080780 c1080779)
|8. (po c1080781 c1080780)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 21
|
|? (po Var91 c1080780)
|
|1. (p c1080780 Var91)
|2. (~ (c (f1075070 c1080780 Var91 Var92) c1080780))
|3. (~ (c (f1075070 c1080780 Var91 Var92) c1080779))
|4. (p c1080779 c1080781)
|5. (~ (pp c1080781 c1080779))
|6. (~ (po c1080781 c1080779))
|7. (~ (ec c1080781 c1080779))
|8. (ntpp c1080780 c1080779)
|9. (po c1080781 c1080780)
|
|> hyp
=============================
Step 22

? (~ (c (f1075070 c1080780 c1080781 Var92) c1080781))

1. (p c1080779 c1080781)
2. (~ (pp c1080781 c1080779))
3. (~ (po c1080781 c1080779))
4. (~ (ec c1080781 c1080779))
5. (ntpp c1080780 c1080779)
6. (po c1080781 c1080780)

> ((~ (c (f1075070 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 23

? (~ (p c1080780 c1080781))

1. (c (f1075070 c1080780 c1080781 Var92) c1080781)
2. (p c1080779 c1080781)
3. (~ (pp c1080781 c1080779))
4. (~ (po c1080781 c1080779))
5. (~ (ec c1080781 c1080779))
6. (ntpp c1080780 c1080779)
7. (po c1080781 c1080780)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 24

? (po c1080781 c1080780)

1. (p c1080780 c1080781)
2. (c (f1075070 c1080780 c1080781 Var92) c1080781)
3. (p c1080779 c1080781)
4. (~ (pp c1080781 c1080779))
5. (~ (po c1080781 c1080779))
6. (~ (ec c1080781 c1080779))
7. (ntpp c1080780 c1080779)
8. (po c1080781 c1080780)

> hyp


LEMMA

The ec(x,z) branch is impossible under po(x,y) and ntpp(y,z).
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp y z)) => (~ (ec x z))))))


> revsk
=============================
Step 2

? (((~ (po c1086964 c1086963)) v (~ (ntpp c1086963 c1086962))) v (~ (ec c1086964 c1086962)))


> hypdisj
=============================
Step 3

? (~ (ec c1086964 c1086962))

1. (ntpp c1086963 c1086962)
2. (po c1086964 c1086963)

> ((~ (ec X Y)) <-- (o X Y))
=============================
Step 4

? (o c1086964 c1086962)

1. (ec c1086964 c1086962)
2. (ntpp c1086963 c1086962)
3. (po c1086964 c1086963)

> ((o X Z) <-- (p Y X) (p Y Z))
|=============================
|Step 5
|
|? (p Var64 c1086964)
|
|1. (~ (o c1086964 c1086962))
|2. (ec c1086964 c1086962)
|3. (ntpp c1086963 c1086962)
|4. (po c1086964 c1086963)
|
|> ((p Z X) <-- (~ (c (f1080843 Z X Y) Z)))
|=============================
|Step 6
|
|? (~ (c (f1080843 Var64 c1086964 Var67) Var64))
|
|1. (~ (p Var64 c1086964))
|2. (~ (o c1086964 c1086962))
|3. (ec c1086964 c1086962)
|4. (ntpp c1086963 c1086962)
|5. (po c1086964 c1086963)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 7
||
||? (p (f1080860 Var70 Var74) Var70)
||
||1. (c (f1080843 (f1080860 Var70 Var74) c1086964 Var67) (f1080860 Var70 Var74))
||2. (~ (p (f1080860 Var70 Var74) c1086964))
||3. (~ (o c1086964 c1086962))
||4. (ec c1086964 c1086962)
||5. (ntpp c1086963 c1086962)
||6. (po c1086964 c1086963)
||
||> ((p (f1080860 X Y) X) <-- (o X Y))
||=============================
||Step 8
||
||? (o Var70 Var74)
||
||1. (~ (p (f1080860 Var70 Var74) Var70))
||2. (c (f1080843 (f1080860 Var70 Var74) c1086964 Var67) (f1080860 Var70 Var74))
||3. (~ (p (f1080860 Var70 Var74) c1086964))
||4. (~ (o c1086964 c1086962))
||5. (ec c1086964 c1086962)
||6. (ntpp c1086963 c1086962)
||7. (po c1086964 c1086963)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 9
||
||? (po Var70 Var74)
||
||1. (~ (o Var70 Var74))
||2. (~ (p (f1080860 Var70 Var74) Var70))
||3. (c (f1080843 (f1080860 Var70 Var74) c1086964 Var67) (f1080860 Var70 Var74))
||4. (~ (p (f1080860 Var70 Var74) c1086964))
||5. (~ (o c1086964 c1086962))
||6. (ec c1086964 c1086962)
||7. (ntpp c1086963 c1086962)
||8. (po c1086964 c1086963)
||
||> hyp
|=============================
|Step 10
|
|? (~ (c (f1080843 (f1080860 c1086964 c1086963) c1086964 Var67) c1086964))
|
|1. (c (f1080843 (f1080860 c1086964 c1086963) c1086964 Var67) (f1080860 c1086964 c1086963))
|2. (~ (p (f1080860 c1086964 c1086963) c1086964))
|3. (~ (o c1086964 c1086962))
|4. (ec c1086964 c1086962)
|5. (ntpp c1086963 c1086962)
|6. (po c1086964 c1086963)
|
|> ((~ (c (f1080843 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 11
|
|? (~ (p (f1080860 c1086964 c1086963) c1086964))
|
|1. (c (f1080843 (f1080860 c1086964 c1086963) c1086964 Var67) c1086964)
|2. (c (f1080843 (f1080860 c1086964 c1086963) c1086964 Var67) (f1080860 c1086964 c1086963))
|3. (~ (p (f1080860 c1086964 c1086963) c1086964))
|4. (~ (o c1086964 c1086962))
|5. (ec c1086964 c1086962)
|6. (ntpp c1086963 c1086962)
|7. (po c1086964 c1086963)
|
|> hyp
=============================
Step 12

? (p (f1080860 c1086964 c1086963) c1086962)

1. (~ (o c1086964 c1086962))
2. (ec c1086964 c1086962)
3. (ntpp c1086963 c1086962)
4. (po c1086964 c1086963)

> ((p Z X) <-- (~ (c (f1080843 Z X Y) Z)))
=============================
Step 13

? (~ (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963)))

1. (~ (p (f1080860 c1086964 c1086963) c1086962))
2. (~ (o c1086964 c1086962))
3. (ec c1086964 c1086962)
4. (ntpp c1086963 c1086962)
5. (po c1086964 c1086963)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 14
|
|? (p (f1080860 c1086964 c1086963) c1086963)
|
|1. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
|2. (~ (p (f1080860 c1086964 c1086963) c1086962))
|3. (~ (o c1086964 c1086962))
|4. (ec c1086964 c1086962)
|5. (ntpp c1086963 c1086962)
|6. (po c1086964 c1086963)
|
|> ((p (f1080860 X Y) Y) <-- (o X Y))
|=============================
|Step 15
|
|? (o c1086964 c1086963)
|
|1. (~ (p (f1080860 c1086964 c1086963) c1086963))
|2. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
|3. (~ (p (f1080860 c1086964 c1086963) c1086962))
|4. (~ (o c1086964 c1086962))
|5. (ec c1086964 c1086962)
|6. (ntpp c1086963 c1086962)
|7. (po c1086964 c1086963)
|
|> ((o X Y) <-- (po X Y))
|=============================
|Step 16
|
|? (po c1086964 c1086963)
|
|1. (~ (o c1086964 c1086963))
|2. (~ (p (f1080860 c1086964 c1086963) c1086963))
|3. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
|4. (~ (p (f1080860 c1086964 c1086963) c1086962))
|5. (~ (o c1086964 c1086962))
|6. (ec c1086964 c1086962)
|7. (ntpp c1086963 c1086962)
|8. (po c1086964 c1086963)
|
|> hyp
=============================
Step 17

? (~ (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086963))

1. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
2. (~ (p (f1080860 c1086964 c1086963) c1086962))
3. (~ (o c1086964 c1086962))
4. (ec c1086964 c1086962)
5. (ntpp c1086963 c1086962)
6. (po c1086964 c1086963)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 18
|
|? (p c1086963 Var94)
|
|1. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086963)
|2. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
|3. (~ (p (f1080860 c1086964 c1086963) c1086962))
|4. (~ (o c1086964 c1086962))
|5. (ec c1086964 c1086962)
|6. (ntpp c1086963 c1086962)
|7. (po c1086964 c1086963)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 19
|
|? (pp c1086963 Var94)
|
|1. (~ (p c1086963 Var94))
|2. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086963)
|3. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
|4. (~ (p (f1080860 c1086964 c1086963) c1086962))
|5. (~ (o c1086964 c1086962))
|6. (ec c1086964 c1086962)
|7. (ntpp c1086963 c1086962)
|8. (po c1086964 c1086963)
|
|> ((pp X Y) <-- (ntpp X Y))
|=============================
|Step 20
|
|? (ntpp c1086963 Var94)
|
|1. (~ (pp c1086963 Var94))
|2. (~ (p c1086963 Var94))
|3. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086963)
|4. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
|5. (~ (p (f1080860 c1086964 c1086963) c1086962))
|6. (~ (o c1086964 c1086962))
|7. (ec c1086964 c1086962)
|8. (ntpp c1086963 c1086962)
|9. (po c1086964 c1086963)
|
|> hyp
=============================
Step 21

? (~ (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086962))

1. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086963)
2. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
3. (~ (p (f1080860 c1086964 c1086963) c1086962))
4. (~ (o c1086964 c1086962))
5. (ec c1086964 c1086962)
6. (ntpp c1086963 c1086962)
7. (po c1086964 c1086963)

> ((~ (c (f1080843 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 22

? (~ (p (f1080860 c1086964 c1086963) c1086962))

1. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086962)
2. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) c1086963)
3. (c (f1080843 (f1080860 c1086964 c1086963) c1086962 Var83) (f1080860 c1086964 c1086963))
4. (~ (p (f1080860 c1086964 c1086963) c1086962))
5. (~ (o c1086964 c1086962))
6. (ec c1086964 c1086962)
7. (ntpp c1086963 c1086962)
8. (po c1086964 c1086963)

> hyp


LEMMA

Proper part splits into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c1093301 c1093300)) v ((tpp c1093301 c1093300) v (ntpp c1093301 c1093300)))


> hypdisj
=============================
Step 3

? (ntpp c1093301 c1093300)

1. (~ (tpp c1093301 c1093300))
2. (pp c1093301 c1093300)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f1087081 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c1093301 c1093300)
|
|1. (~ (ntpp c1093301 c1093300))
|2. (~ (tpp c1093301 c1093300))
|3. (pp c1093301 c1093300)
|
|> hyp
=============================
Step 5

? (~ (ec (f1087081 c1093301 c1093300 Var32) c1093301))

1. (~ (ntpp c1093301 c1093300))
2. (~ (tpp c1093301 c1093300))
3. (pp c1093301 c1093300)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c1093301 Var36)
||
||1. (ec (f1087081 c1093301 c1093300 Var32) c1093301)
||2. (~ (ntpp c1093301 c1093300))
||3. (~ (tpp c1093301 c1093300))
||4. (pp c1093301 c1093300)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f1087081 c1093301 c1093300 Var32) c1093300)
|
|1. (ec (f1087081 c1093301 c1093300 Var32) c1093301)
|2. (~ (ntpp c1093301 c1093300))
|3. (~ (tpp c1093301 c1093300))
|4. (pp c1093301 c1093300)
|
|> ((ec (f1087081 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c1093301 c1093300))
||
||1. (~ (ec (f1087081 c1093301 c1093300 Var32) c1093300))
||2. (ec (f1087081 c1093301 c1093300 Var32) c1093301)
||3. (~ (ntpp c1093301 c1093300))
||4. (~ (tpp c1093301 c1093300))
||5. (pp c1093301 c1093300)
||
||> hyp
|=============================
|Step 9
|
|? (pp c1093301 c1093300)
|
|1. (~ (ec (f1087081 c1093301 c1093300 Var32) c1093300))
|2. (ec (f1087081 c1093301 c1093300 Var32) c1093301)
|3. (~ (ntpp c1093301 c1093300))
|4. (~ (tpp c1093301 c1093300))
|5. (pp c1093301 c1093300)
|
|> hyp
=============================
Step 10

? (~ (tpp c1093301 c1093300))

1. (ec (f1087081 c1093301 c1093300 Var32) c1093301)
2. (~ (ntpp c1093301 c1093300))
3. (~ (tpp c1093301 c1093300))
4. (pp c1093301 c1093300)

> hyp


LEMMA

Use Lemma8 and eliminate ec with Lemma9. Then split pp into tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp y z)) => (((po x z) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (po c1099791 c1099790)) v (~ (ntpp c1099790 c1099789))) v (((po c1099791 c1099789) v (tpp c1099791 c1099789)) v (ntpp c1099791 c1099789)))


> hypdisj
=============================
Step 3

? (ntpp c1099791 c1099789)

1. (~ (tpp c1099791 c1099789))
2. (~ (po c1099791 c1099789))
3. (ntpp c1099790 c1099789)
4. (po c1099791 c1099790)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c1099791 c1099789)
|
|1. (~ (ntpp c1099791 c1099789))
|2. (~ (tpp c1099791 c1099789))
|3. (~ (po c1099791 c1099789))
|4. (ntpp c1099790 c1099789)
|5. (po c1099791 c1099790)
|
|> ((pp Y Z) <-- (po Y X) (ntpp X Z) (~ (ec Y Z)) (~ (po Y Z)))
||||=============================
||||Step 5
||||
||||? (po c1099791 Var35)
||||
||||1. (~ (pp c1099791 c1099789))
||||2. (~ (ntpp c1099791 c1099789))
||||3. (~ (tpp c1099791 c1099789))
||||4. (~ (po c1099791 c1099789))
||||5. (ntpp c1099790 c1099789)
||||6. (po c1099791 c1099790)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (ntpp c1099790 c1099789)
|||
|||1. (~ (pp c1099791 c1099789))
|||2. (~ (ntpp c1099791 c1099789))
|||3. (~ (tpp c1099791 c1099789))
|||4. (~ (po c1099791 c1099789))
|||5. (ntpp c1099790 c1099789)
|||6. (po c1099791 c1099790)
|||
|||> hyp
||=============================
||Step 7
||
||? (~ (ec c1099791 c1099789))
||
||1. (~ (pp c1099791 c1099789))
||2. (~ (ntpp c1099791 c1099789))
||3. (~ (tpp c1099791 c1099789))
||4. (~ (po c1099791 c1099789))
||5. (ntpp c1099790 c1099789)
||6. (po c1099791 c1099790)
||
||> ((~ (ec X Z)) <-- (po X Y) (ntpp Y Z))
|||=============================
|||Step 8
|||
|||? (po c1099791 Var40)
|||
|||1. (ec c1099791 c1099789)
|||2. (~ (pp c1099791 c1099789))
|||3. (~ (ntpp c1099791 c1099789))
|||4. (~ (tpp c1099791 c1099789))
|||5. (~ (po c1099791 c1099789))
|||6. (ntpp c1099790 c1099789)
|||7. (po c1099791 c1099790)
|||
|||> hyp
||=============================
||Step 9
||
||? (ntpp c1099790 c1099789)
||
||1. (ec c1099791 c1099789)
||2. (~ (pp c1099791 c1099789))
||3. (~ (ntpp c1099791 c1099789))
||4. (~ (tpp c1099791 c1099789))
||5. (~ (po c1099791 c1099789))
||6. (ntpp c1099790 c1099789)
||7. (po c1099791 c1099790)
||
||> hyp
|=============================
|Step 10
|
|? (~ (po c1099791 c1099789))
|
|1. (~ (pp c1099791 c1099789))
|2. (~ (ntpp c1099791 c1099789))
|3. (~ (tpp c1099791 c1099789))
|4. (~ (po c1099791 c1099789))
|5. (ntpp c1099790 c1099789)
|6. (po c1099791 c1099790)
|
|> hyp
=============================
Step 11

? (~ (tpp c1099791 c1099789))

1. (~ (ntpp c1099791 c1099789))
2. (~ (tpp c1099791 c1099789))
3. (~ (po c1099791 c1099789))
4. (ntpp c1099790 c1099789)
5. (po c1099791 c1099790)

> hyp
